{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": { "collapsed": false }, "outputs": [], "source": [ "import random\n", "from IPython.core.display import SVG\n", "import pyomo.environ as p\n", "from pysat.solvers import Solver\n", "from pysat.formula import CNF\n", "import py_svg_combinatorics as psc\n", "from ipywidgets import widgets, HBox\n", "from collections import Counter\n", "from pprint import pprint\n", "from random import randint\n", "import numpy as np\n", "from IPython.display import IFrame\n", "import IPython\n", "from copy import copy\n", "import os\n", "from pathlib import Path\n", "from collections import defaultdict\n", "from itertools import combinations\n", "import time\n" ] }, { "cell_type": "code", "execution_count": 2, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/html": [ "\n", " \n", " " ], "text/plain": [ "" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "from IPython.display import IFrame\n", "title_ = 'Minimum Test Collection'\n", "IFrame(f'https://discopal.ispras.ru/index.php?title=Hardprob/{title_}&useskin=cleanmonobook', width=1280, height=700)" ] }, { "cell_type": "code", "execution_count": 3, "metadata": { "collapsed": false }, "outputs": [], "source": [ "model = p.ConcreteModel()" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "# Визуализация" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Без ограничения общности, пусть у нас подмножество $S$ – численное." ] }, { "cell_type": "code", "execution_count": 4, "metadata": { "collapsed": false }, "outputs": [], "source": [ "model.InitialSet = range(10)\n", "model.SetLen = len(model.InitialSet)\n", "model.SetIndex = range(model.SetLen)" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Зададим семейство подмножеств $С$:" ] }, { "cell_type": "code", "execution_count": 5, "metadata": { "collapsed": false }, "outputs": [], "source": [ "model.InitialSubsets = [[1,2], [1,2,3], [5,6], [6,8,], [0,4,7], [0,1,2,3,4,5,6,7,8,9], [0], [1], [2], [5,7]]" ] }, { "cell_type": "code", "execution_count": 6, "metadata": { "collapsed": false }, "outputs": [ { "data": { "image/svg+xml": [ "\n", " \n", " \n", " \n", "" ], "text/plain": [ "" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "svg = psc.subsets2svg(model.InitialSubsets)\n", "SVG(data=svg)" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Запомним его мощность и проиндексируем подмножества." ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "collapsed": false }, "outputs": [], "source": [ "model.SubsetCount = len(model.InitialSubsets)\n", "model.SubsetIndex = range(model.SubsetCount)" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Удобнее будет хранить его в виде таблицы связности: \n", "\n", "$S[i][j] = 1$, если $i$-ое подмножество содержит элемент $j$" ] }, { "cell_type": "code", "execution_count": 8, "metadata": { "collapsed": false }, "outputs": [], "source": [ "S = [[0 for _ in range(model.SetLen)] for _ in range(model.SubsetCount)]\n", "\n", "for i in range(model.SubsetCount):\n", " for elem in model.InitialSubsets[i]:\n", " S[i][elem] = 1\n", "\n", "model.Subsets = S" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "# Реализация в Pyomo" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "**Переменная** $x[i] = 1$, если мы берем $i$ подмножество в целевое семейство $C'$ и $0$ в противном случае." ] }, { "cell_type": "code", "execution_count": 9, "metadata": { "collapsed": false }, "outputs": [], "source": [ "model.x = p.Var(model.SubsetIndex, within=p.Binary)" ] }, { "cell_type": "code", "execution_count": 10, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def display_model(model):\n", " selected_sets = [subset for subset in model.SubsetIndex if round(model.x[subset]()) == 1]\n", " return SVG(psc.subsets2svg(model.InitialSubsets, selected=selected_sets))" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "**Целевая функция** — мощность семейства $C'$, т.е. сумма $x[i]$ по $i$" ] }, { "cell_type": "code", "execution_count": 11, "metadata": { "collapsed": false }, "outputs": [], "source": [ "@model.Objective()\n", "def FinalCapacity(model):\n", " return sum(model.x[subset] for subset in model.SubsetIndex)" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Единственное ограничение:\n", "\n", "$$ \\forall i,j \\in S\\; \\exists C_k \\in C':\n", "\\left[ \n", " \\begin{gathered} \n", "\t\ti \\in C_k, j \\notin C_k, \\\\ \n", "\t\ti \\notin C_k, j \\in C_k \\\\\n", " \\end{gathered} \n", "\\right.\n", "$$\n", "\n", "\n", "То есть\n", "\n", "$$\\forall i,j \\in S \\exists C_k \\in C':\\; Subsets\\left[C_k\\right]\\left[i\\right] XOR \\;Subsets\\left[C_k\\right]\\left[j\\right] == 1$$" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Теперь можно просто заменить существование на сравнение суммы по k с единицей." ] }, { "cell_type": "code", "execution_count": 12, "metadata": { "collapsed": false }, "outputs": [], "source": [ "@model.Constraint(model.SetIndex, model.SetIndex)\n", "def all_pair_of_elements_are_included_excluded(model, i, j):\n", " if i <= j:\n", " return p.Constraint.Feasible\n", " else:\n", " return sum(model.x[subset] * (model.Subsets[subset][i] ^ model.Subsets[subset][j]) for subset in model.SubsetIndex) >= 1" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Определяем солвер:" ] }, { "cell_type": "code", "execution_count": 13, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "# ==========================================================\n", "# = Solver Results =\n", "# ==========================================================\n", "# ----------------------------------------------------------\n", "# Problem Information\n", "# ----------------------------------------------------------\n", "Problem: \n", "- Name: unknown\n", " Lower bound: 8.0\n", " Upper bound: 8.0\n", " Number of objectives: 1\n", " Number of constraints: 3\n", " Number of variables: 3\n", " Number of binary variables: 10\n", " Number of integer variables: 10\n", " Number of nonzeros: 3\n", " Sense: minimize\n", "# ----------------------------------------------------------\n", "# Solver Information\n", "# ----------------------------------------------------------\n", "Solver: \n", "- Status: ok\n", " User time: -1.0\n", " System time: 0.01\n", " Wallclock time: 0.01\n", " Termination condition: optimal\n", " Termination message: Model was solved to optimality (subject to tolerances), and an optimal solution is available.\n", " Statistics: \n", " Branch and bound: \n", " Number of bounded subproblems: 0\n", " Number of created subproblems: 0\n", " Black box: \n", " Number of iterations: 0\n", " Error rc: 0\n", " Time: 0.49807310104370117\n", "# ----------------------------------------------------------\n", "# Solution Information\n", "# ----------------------------------------------------------\n", "Solution: \n", "- number of solutions: 0\n", " number of solutions displayed: 0\n" ] } ], "source": [ "solver = p.SolverFactory('cbc')\n", "solver.solve(model).write()" ] }, { "cell_type": "code", "execution_count": 14, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "[0, 1, 2, 3, 4, 6, 8, 9]" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "selected_sets = [subset for subset in model.SubsetIndex if round(model.x[subset]()) == 1]\n", "selected_sets" ] }, { "cell_type": "code", "execution_count": 15, "metadata": { "collapsed": false }, "outputs": [ { "data": { "image/svg+xml": [ "\n", " \n", " \n", " \n", "" ], "text/plain": [ "" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "display_model(model)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "**StasFomin**: Увы, моя вина, что нечетко (хотя однозначно, как в базе Вигго-Кана) сформулировал. Сейчас обновил формулировку, пояснив примером, о чем эта задача — т.е. это как покрытие, но с дополнительными ограничениями на различимость болезней. Увы, тут уже видно, что «9»-я болезнь не покрывается никакими тестами." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "~~~~: Ну, увы, тут уже видно, что выбранный набор не сможет быть «тестом» для выбранного набора «болезней», ибо 9я болезнь не детектируется ничем. Т.е. эта задача как покрытие, но с дополнительными ограничениями на возможность различить болезни. Моя вина, что нечетко это сформулировал (ну так было в оригинале), но увы." ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Модель в общем случае:" ] }, { "cell_type": "code", "execution_count": 16, "metadata": { "collapsed": false }, "outputs": [], "source": [ "\n", "def MNT_ILP_model(initial_set, initial_subsets):\n", " \"\"\"initial_set -- range(k) или range(a, b) со сдвигом\"\"\"\n", " model = p.ConcreteModel()\n", " \n", " model.InitialSet = initial_set\n", " model.SetLen = len(model.InitialSet)\n", " model.SetIndex = range(model.SetLen)\n", " \n", " model.SubsetCount = len(initial_subsets)\n", " model.SubsetIndex = range(model.SubsetCount)\n", "\n", " # model.InitialSubsets -- значения initial_subsets после сдвига \n", " # range(a, b) -> range(b-a), для этого вычитаем из каждого элемента min.\n", " _min = min(model.InitialSet)\n", " model.InitialSubsets = [[elem - _min for elem in subset] for subset in initial_subsets]\n", "\n", " S = [[0 for _ in range(model.SetLen)] for _ in range(model.SubsetCount)]\n", "\n", " for i in range(model.SubsetCount):\n", " for elem in model.InitialSubsets[i]:\n", " S[i][elem] = 1\n", "\n", " model.Subsets = S\n", "\n", " model.x = p.Var(model.SubsetIndex, within=p.Binary)\n", " \n", " @model.Objective()\n", " def FinalCapacity(model):\n", " return sum(model.x[subset] for subset in model.SubsetIndex)\n", "\n", " @model.Constraint(model.SetIndex, model.SetIndex)\n", " def all_pair_of_elements_are_included_excluded(model, i, j):\n", " if i <= j:\n", " return p.Constraint.Feasible\n", " else:\n", " return sum(model.x[subset] * (model.Subsets[subset][i] ^ model.Subsets[subset][j]) for subset in model.SubsetIndex) >= 1\n", "\n", " return model" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "### Трансляция к задаче о разрешимости\n", "Если мощность найденного $ C' \\subseteq C $ меньше, либо равна, заданного параметра $\\gamma(|C|)$, то задача разрешима. Иначе нет." ] }, { "cell_type": "code", "execution_count": 17, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def is_feasible_pyomo(initial_set, initial_subsets, gamma):\n", " model = MNT_ILP_model(initial_set, initial_subsets)\n", "\n", " solver = p.SolverFactory('cbc')\n", " try:\n", " solution = solver.solve(model)\n", "\n", " if str(solution['Solver'][0]['Termination condition']) == 'optimal' and model.FinalCapacity() <= gamma:\n", " return True, model\n", " else:\n", " return False, None\n", " except:\n", " return False, None" ] }, { "cell_type": "code", "execution_count": 18, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "WARNING: Loading a SolverResults object with a warning status into\n", "model.name=\"unknown\";\n", " - termination condition: infeasible\n", " - message from solver: \n" ] }, { "data": { "text/plain": [ "False" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "is_feasible_pyomo(gamma=100, initial_set=range(5), initial_subsets=[[0,1], [1]])[0]" ] }, { "cell_type": "code", "execution_count": 19, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "is_feasible_pyomo(gamma = 4, initial_set=range(5), initial_subsets=[[0,1], [1], [2], [3], [4]])[0]" ] }, { "cell_type": "code", "execution_count": 20, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "False" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "is_feasible_pyomo(gamma = 3, initial_set=range(5), initial_subsets=[[0,1], [1], [2], [3], [4]])[0]" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "# Сведение 3SAT к задаче" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Пусть нам дана формула \n", "$$\\Phi(x_1, y_1, z_1, \\dots, x_p, y_p, z_p) = \\varphi_1(x_1,y_1,z_1) \\bigwedge \\varphi_2(x_2,y_2,z_2) \\dots \\varphi_p(x_p,y_p,z_p)$$\n", "Здесь $\\varphi_1(x_1,y_1,z_1) = x_1 \\bigvee y_1 \\bigvee z_1$ – конъюкция и $x_1, y_1, z_1$ – булевы литералы, либо их отрицание (например, $\\varphi_1(x_1, \\overline{x_4}, \\overline{x_6})$).\n", "\n", "Пусть в $\\Phi$ входит **p** конъюкций и **k** независимых булевых переменных (не считая их отрицаний)." ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "### Строим по 3SAT условие для MNT\n", "\n", "Исходное множество значений $\\textbf{C}$ для задачи Minimum Test Collection(MNT) будет состоять из следующих элементов:\n", "- \"0\" — вспомогательный нулевой элемент, не входит ни в одно подмножество семейства $\\textbf{C}$,\n", "- \"$+\\infty$\" — вспомогательный элемент, содержится ровно в одном подмножестве $\\textbf{C}$,\n", "- \"$\\{-1, -2, -3, \\dots, -k\\}$\" — \"ядра\" булевых переменных,\n", "- \"$\\{1, 1.5, 2, 2.5, \\dots, p, p + 0.5 \\}$\" — \"ядра\" конъюкций (целые) и вспомогательные элементы (дробные)." ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Строим исходное семейство подмножеств $\\textbf{C}$. В него будут входить следующие подмножества:\n", "- \"черное\" — содержит $+\\infty$ и все положительные числа. $\\textbf{N} = \\{+\\infty, 1, 1.5, \\dots, p, p + 0.5\\} \\in \\textbf{C}$,\n", "- \"красные\" — $p$ подмножеств, содержащих ровно 2 элемента: $i$ и $i + 0.5$. $\\textbf{R} = \\Big\\{ \\textbf{r} |\\; \\textbf{r} = \\big\\{ i, i + 0.5 \\big\\}, i \\in \\overline{1\\dots p} \\Big\\} \\subset \\textbf{C}$ \n", "- \"синие\" — $2k$ подмножеств, половина которых содержит число $-i$ и $conj_i$ (назовем их $\\textbf{x}_\\textbf{i}$), а вторая половина — $-i$ и $\\overline{conj_i}$ (назовем их $\\overline{\\textbf{x}_\\textbf{i}}$). $\\textbf{B} = \\Big\\{ \\textbf{x}_\\textbf{i} |\\; \\textbf{x}_\\textbf{i} = \\{ -i \\} \\cup conj_i, i \\in \\overline{1..k} \\Big\\} \\cup \\Big\\{ \\overline{\\textbf{x}_\\textbf{i}} |\\; \\overline{\\textbf{x}_\\textbf{i}} = \\{ -i \\} \\cup \\overline{conj_i}, i \\in \\overline{1..k} \\Big\\} \\subset \\textbf{C}$" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "#### **Утверждение:** \n", "Существование решения задачи Minimum Test Collection(MNT) с построенными $\\textbf{S}$, $\\textbf{C}$ и $gamma = 1 + p + k$ эквивалентно существованию решения 3-SAT: $\\Phi(x_1, \\overline{x_1}, x_2, \\overline{x_2}, \\dots, x_k, \\overline{x_k}) = 1$.\n", "\n", "
или
\n", "\n", "$$ \\exists C' \\text{ -- решение MNT}(S,C,gamma) \\Longleftrightarrow \\exists \\{x^*_1, x^*_2, \\dots x^*_k\\} \\text{ -- решение 3SAT: } \\Phi(x_1, \\overline{x_1}, x_2, \\overline{x_2}, \\dots, x_k, \\overline{x_k}) = 1 $$" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "#### **Доказательство:**" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "**Влево:**\n", "Пусть набор $ \\{x^*_1, x^*_2, \\dots x^*_k\\} \\text{ -- решение 3SAT: } \\Phi(x_1, \\overline{x_1}, x_2, \\overline{x_2}, \\dots, x_k, \\overline{x_k}) = 1 $. \\\n", "Решим MNT с заданными $\\textbf{S}, \\textbf{C}$ и $gamma = 1 + p + k$. Выберем из $\\textbf{C}$ следующие подмножества:\n", "- \"черное\",\n", "- все \"красные\",\n", "- \"синие\" по следующему правилу: для каждого $i \\in \\overline{1..k}$, если $x^*_i = 1$ — берем $\\{-i \\} \\cup conj_i \\in \\textbf{B}$, если $x^*_i = 0$ — берем $\\{-i \\} \\cup \\overline{conj_i} \\in \\textbf{B}$\n", "\n", "Итого $ |C'| = 1 + p + k $ подмножеств выбрано.\n", "\n", "Докажем, что такой выбор подмножеств удовлетворяет условию MNT:\\\n", "Покажем, что каждый элемент из $\\textbf{S}$ ни конфликтует ни с каким другим (т.е. для любой пары есть подмножество из |C'|, содержащее один элемент, но не второй):\n", "- Нулевой элемент\n", " - $+\\infty$: входит в \"черное\", а \"0\" — нет,\n", " - Отрицательные числа: $\\forall i \\in \\overline{1..k}$ вы взяли \"синее\", содержащее $-i$, но не \"0\",\n", " - Положительные числа: каждое положительное число входит в \"красное\", куда не входит \"0\", \"красные\" взяли все.\n", "- $+\\infty$\n", " - Отрицательные числа: не входят в \"черное\", куда входит $+\\infty$,\n", " - Положительные числа: каждое положительное число входит в \"красное\", куда не входит $+\\infty$, \"красные\" взяли все.\n", "- Отрицательные числа\n", " - Другие отрицательные: $\\forall i \\in \\overline{1..k}$ вы взяли \"синее\", содержащее единственное отрицательное число: $-i$,\n", " - Положительные числа: входят в \"черное\", куда не входят отрицательные.\n", "- Дробные положительные:\n", " - Другие дробные: в каждом \"красном\" ровно одно дробное число, \"красные\" взяли все.\n", " - Целые положительные (не из \"красного\", в которое входит исходное дробное): берем это \"красное\".\n", "- Целые положительные:\n", " - Другие целые положительные: в каждом \"красном\" ровно одно целое число, \"красные\" взяли все. " ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Итак, не разобрана только одна связь: дробные положительные и целые положительные, входящие в одно \"красное\" подмножество.\\\n", "Пусть в 3SAT-задаче $\\varphi_i = x_a \\bigvee x_b \\bigvee x_c$. Тогда, по построению, целое число $i$, помимо 1 \"черного\" и 1 \"красного\" подмножества, потенциально входит в 3 \"синих\": в те, что содержат числа $-a, -b, -c$ ($\\{-a\\} \\cup conj_a$ и т.д.). При этом, исходная задача разрешима, значит $x^*_a = 1$, или $x^*_b = 1$, или $x^*_c = 1$, значит, по построению \"синих\", мы выбрали в $C'$ одно из этих трёх \"синих\". Таким образом это \"синее\" подмножество разрешает конфликт между $i$ и $i + 0.5$.\n", "\n", "**Замечание**: если $\\varphi_i = \\overline{x_a} \\bigvee x_b \\bigvee \\overline{x_c}$, идея выше не поменяется, в таком случае $x^*_a = 0$, или $x^*_b = 1$, или $x^*_c = 0$ и $i$ входит в одно из ($\\{-a\\} \\cup \\overline{conj_a}$, или $\\{-b\\} \\cup conj_b$, или $\\{-c\\} \\cup \\overline{conj_c}$)." ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "**Вправо:**\n", "\n", "Пусть $C'$ — решение MNT( $\\mathbf{S}$, $\\mathbf{C}$, $gamma = 1 + p + k$).\\\n", "Заметим, что исходя из построенного $\\mathbf{S}$ и $\\mathbf{C}$, чтобы не было конфликтов между элементами $\\mathbf{S}$:\n", "1) \"Черное\" подмножество входит в $C'$, иначе конфликт между \"0\" и $+\\infty$ (\"0\" не входит ни в одно, $+\\infty$ входит только в \"черное\" ).\n", "2) Чтобы исключить конфликт между $+\\infty$ и дробными положительными, а так как каждое дробного положительного входит только в \"черное\" (что не решает конфликт) и в одно \"красное\", необходимо внести все \"красные\" в $C'$.\\\n", "**Мы уже потратили $1 + p$ подмножеств.**\n", "3) Чтобы исключить конфликт между \"0\" и отрицательными числами, для каждого $i \\in \\overline{1..k}$ необходимо взять в $C'$ либо $\\textbf{x}_\\textbf{i} = \\{-i\\} \\cup conj_i$, либо $\\overline{\\textbf{x}_\\textbf{i}} = \\{-i\\} \\cup \\overline{conj_i}$.\\\n", "При этом нам осталось доступно только $gamma - 1 - p = k$ подмножеств, значит для каждого $i \\in \\overline{1..k}$ надо взять одно и ровно одно: $\\textbf{x}_\\textbf{i}$ или $\\overline{\\textbf{x}_\\textbf{i}}$.\n", "4) Чтобы устранить конфликт между дробными и целыми положительными, находящимися в одной \"красной\" (т.е. между $i$ и $i + 0.5$), для каждого $i \\in \\overline{1..p}$ в $C'$ должно быть хотя бы одно \"синее\" подмножество, содержащее $i$." ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Докажем, что из этих выводов следует, что набор $\\{x^*_1, x^*_2, \\dots x^*_k\\}$, где\n", "\\begin{equation}\n", "x^*_i = \n", "\t\\begin{cases}\n", "\t\t1 &, \\text{мы выбрали }\\textbf{x}_\\textbf{i} (\\textbf{x}_\\textbf{i} \\in C' )\\\\\n", " 0 &, \\text{мы выбрали } \\overline{\\textbf{x}_\\textbf{i}} (\\overline{\\textbf{x}_\\textbf{i}} \\in C')\n", "\t\\end{cases}\n", "\\end{equation}\n", "является решением исходной 3SAT.\n", "\n", "Из (3) следует, что $x^*_i$ определяется однозначно $\\forall i \\in \\overline{1..k}$.\\\n", "Из (4) следует, что $\\forall i \\in \\overline{1..p}\\; \\exists$ хотя бы одно \"синее\" подмножество, содержащее $i$, лежащее в $C'$. Пусть это синее подмножество сформировано вокруг элемента $-k\\_i$, то есть это $\\textbf{x}_\\textbf{k\\_i}$, если $x_{k\\_i}$ входит в $\\varphi_i$, либо $\\overline{\\textbf{x}_\\textbf{k\\_i}}$, если в $\\varphi_i$ входит $\\overline{x_{k\\_i}}$ . Таким образом:\n", "$$ \\left[ \n", "\t\\begin{gathered} \n", "\t\t\\forall i \\in \\overline{1..p} \\; \\exists \\textbf{x}_\\textbf{k\\_i} \\in C':\\; x_{k\\_i} \\in \\varphi_i \\\\\n", "\t\t\\forall i \\in \\overline{1..p} \\; \\exists \\overline{\\textbf{x}_\\textbf{k\\_i}} \\in C':\\; \\overline{x_{k\\_i}} \\in \\varphi_i\n", "\t\\end{gathered} \n", "\\right.$$\n", "\n", "То есть для каждой конъюкции $\\varphi_i$ из $\\Phi = \\varphi_1 \\wedge \\varphi_2 \\wedge \\dots \\wedge \\varphi_p$ (т.е. для каждого положительного целого элемента) есть хотя бы один элемент $x^*_{k\\_i} = 1$ (либо $\\overline{x^*_{k\\_i}} = \\overline{0} = 1$), входящий в эту конъюкцию, значит все конъюкции выполняются, значит $\\{x^*_1, x^*_2, \\dots x^*_k\\}$ — решение $\\Phi = 1$." ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "### Визуализируем" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Функция, генерирующая рандомную формулу 3-КНФ " ] }, { "cell_type": "code", "execution_count": 21, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def Generate_random_3cnf(seed, conjunction_count, variables_count):\n", " random.seed(seed)\n", " return CNF(from_clauses=psc.rand3cnf(conjunction_count, variables_count))" ] }, { "cell_type": "code", "execution_count": 22, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "[(-2, 5, 4), (-3, 1, 5), (3, 5, -4), (5, 3, -1)]" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "cnf = Generate_random_3cnf(3, 4, 5)\n", "cnf.clauses" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Функция, превращающая любую 3-КНФ формулу в экземляр задачи MNT (тройку (S, C, gamma)) по алгоритму, описанному выше.\n" ] }, { "cell_type": "code", "execution_count": 23, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def transform_3cnf_to_MNT(cnf3):\n", " clauses = cnf3.clauses\n", "\n", " var_names = set()\n", " for clause in clauses:\n", " for var in clause:\n", " var_names.add(abs(var))\n", " # psc.rand3cnf всегда называет переменные в порядке от 1 до k (без пробелов)\n", " \n", " # Число переменных k\n", " k = len(var_names)\n", " # Число конъюкций p\n", " p = len(clauses)\n", " # Параметр gamma\n", " gamma = 1 + k + p\n", "\n", " # Исходное множество значений S.\n", " # Для простоты положительные числа умножены на 2 и уменьшины на 1 (теперь они не range(1, p + 0.5, step=0.5), а range(1, 2p + 1)),\n", " # роль infty выполняет 2p + 1.\n", " S = list(range(-k, 0)) + [0] + list(range(1, 2 * p + 1 )) + [2 * p + 1]\n", " # Исходное семейство подмножеств С.\n", " C = []\n", " # Добавляем \"черное\"\n", " C.append(list(range(1, 2 * p + 2)))\n", " # Добавляем \"красные\"\n", " for i in range(0, p):\n", " C.append([2 * i + 1, 2 * (i + 1)])\n", " # Добавляем \"синие\"\n", " var_in_conj, non_var_in_conj = [[-i] for i in range(1, k + 1)], [[-i] for i in range(1, k + 1)]\n", " for conj_id, clause in enumerate(clauses):\n", " for var in clause:\n", " if var > 0:\n", " # var_in_conj[0] = [-1]\n", " var_in_conj[abs(var) - 1].append(2 * conj_id + 1)\n", " else:\n", " non_var_in_conj[abs(var) - 1].append(2 * conj_id + 1)\n", " C.extend(var_in_conj)\n", " C.extend(non_var_in_conj)\n", " return S, C, gamma" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Пример того, что выдает эта функция." ] }, { "cell_type": "code", "execution_count": 24, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Исходная задача: [(-1, -2), (1, -2), (2, -1)]\n", "initial_set: [-2, -1, 0, 1, 2, 3, 4, 5, 6, 7]\n", "initial_subsets: [[1, 2, 3, 4, 5, 6, 7], [1, 2], [3, 4], [5, 6], [-1, 3], [-2, 5], [-1, 1, 5], [-2, 1, 3]]\n", "gamma: 6\n" ] } ], "source": [ "cnf3 = Generate_random_3cnf(seed=1, conjunction_count=3, variables_count=2)\n", "\n", "print(f'Исходная задача: {cnf3.clauses}')\n", "\n", "(initial_set, initial_subsets, gamma) = transform_3cnf_to_MNT(cnf3)\n", "\n", "print(f'initial_set: {initial_set}')\n", "print(f'initial_subsets: {initial_subsets}')\n", "print(f'gamma: {gamma}')\n", "\n", "(is_feasible, model) = is_feasible_pyomo(\n", " initial_set, initial_subsets, gamma\n", ")" ] }, { "cell_type": "code", "execution_count": 25, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "selected_subsets: [[1, 2, 3, 4, 5, 6, 7], [1, 2], [3, 4], [5, 6], [-1, 1, 5], [-2, 1, 3]]\n" ] }, { "data": { "image/svg+xml": [ "\n", " \n", " \n", " \n", "" ], "text/plain": [ "" ] }, "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ "if is_feasible:\n", " selected_subsets = [initial_subsets[subset] for subset in model.SubsetIndex if round(model.x[subset]()) == 1]\n", " print(f'selected_subsets: {selected_subsets}')\n", " svg = display_model(model)\n", "svg" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "# Проверка выполнимости через ЦЛП и SAT-Solver" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Проверка разрешимости 3-КНФ через преобразование к MNT и решение через pyomo-ЦЛП" ] }, { "cell_type": "code", "execution_count": 26, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def is_feasible_ILP(cnf3):\n", " (initial_set, initial_subsets, gamma) = transform_3cnf_to_MNT(cnf3)\n", " return is_feasible_pyomo(initial_set, initial_subsets, gamma)[0]" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Проверка разрешимости 3-КНФ через pysat Solver" ] }, { "cell_type": "code", "execution_count": 27, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def is_feasible_SAT(cnf3):\n", " from pysat.solvers import Solver\n", "\n", " solver = Solver(bootstrap_with=cnf3)\n", " return solver.solve() " ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Проверим что это вообще работает на тривиальных 3-КНФ." ] }, { "cell_type": "code", "execution_count": 28, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "(True, False, True, False)" ] }, "execution_count": 28, "metadata": {}, "output_type": "execute_result" } ], "source": [ "true_cnf = CNF(from_clauses=[(1,2,3), (1,-2,-3), (1,2,-3)])\n", "false_cnf = CNF(from_clauses=[(1,2,3), (1,2,-3), (1,-2, 3), (1,-2,-3), (-1,2,3), (-1,2,-3), (-1,-2, 3), (-1,-2,-3),])\n", "\n", "is_feasible_SAT(true_cnf), is_feasible_SAT(false_cnf), is_feasible_ILP(true_cnf), is_feasible_ILP(false_cnf), " ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Тест, который генерирует $test\\_length$ случайных 3-КНФ формул длины до $max\\_conj\\_count$ и проверяет, что наш ILP и pysat солвер выдают один и тот же ответ на задачу разрешимости" ] }, { "cell_type": "code", "execution_count": 29, "metadata": { "collapsed": false }, "outputs": [], "source": [ "\n", "def run_test(test_length, max_conj_count):\n", " start = time.time()\n", " misses_count = 0\n", " for _ in range(test_length):\n", " seed = randint(0, 10_000_000)\n", " conj_count = randint(1, max_conj_count)\n", " var_count = randint(1, max(1, conj_count // 3))\n", " Phi = Generate_random_3cnf(seed=seed, conjunction_count=conj_count, variables_count=var_count)\n", "\n", " if is_feasible_ILP(Phi) != is_feasible_SAT(Phi):\n", " misses_count += 1\n", " if misses_count % 5 == 0:\n", " print(\"Got 5 misses\")\n", " return misses_count, time.time() - start" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Теперь просто гоняем тесты" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Тест на больших формул:" ] }, { "cell_type": "code", "execution_count": 30, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "(0, 12.412810325622559)" ] }, "execution_count": 30, "metadata": {}, "output_type": "execute_result" } ], "source": [ "run_test(10, 50)" ] }, { "cell_type": "code", "execution_count": 31, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "(0, 156.25865602493286)" ] }, "execution_count": 31, "metadata": {}, "output_type": "execute_result" } ], "source": [ "run_test(120, 50)" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Много тестов для формулы поменьше:" ] }, { "cell_type": "code", "execution_count": 32, "metadata": { "collapsed": false }, "outputs": [ { "data": { "text/plain": [ "(0, 100.30018091201782)" ] }, "execution_count": 32, "metadata": {}, "output_type": "execute_result" } ], "source": [ "run_test(500, 10)" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Судя по результатам, для всех прогнанных тестов задачи были эквивалентны." ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Теперь хочется прогнать на совсем больших формулах (и посмотреть, что задачка действительно $NP$: с увеличением входа время растет экспоненциально)." ] }, { "cell_type": "code", "execution_count": 33, "metadata": { "collapsed": false }, "outputs": [], "source": [ "def big_test(conj_count):\n", " mark1 = time.time()\n", "\n", " Phi = Generate_random_3cnf(seed=randint(0,1_000_000), conjunction_count=conj_count, variables_count=conj_count)\n", " mark2 = time.time()\n", "\n", " ILP_res = is_feasible_ILP(Phi)\n", " mark3 = time.time()\n", "\n", " SAT_res = is_feasible_SAT(Phi)\n", " mark4 = time.time()\n", "\n", " if ILP_res != SAT_res:\n", " print(\"Err\")\n", " else:\n", " print(\"Ok\")\n", " return mark2 - mark1, mark3 - mark2, mark4 - mark3" ] }, { "cell_type": "code", "execution_count": 34, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Ok\n" ] }, { "data": { "text/plain": [ "(0.005578756332397461, 11.565046072006226, 0.0005283355712890625)" ] }, "execution_count": 34, "metadata": {}, "output_type": "execute_result" } ], "source": [ "big_test(50)" ] }, { "cell_type": "code", "execution_count": 35, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Ok\n" ] }, { "data": { "text/plain": [ "(0.06852245330810547, 77.0499587059021, 0.00041866302490234375)" ] }, "execution_count": 35, "metadata": {}, "output_type": "execute_result" } ], "source": [ "big_test(100)" ] }, { "cell_type": "code", "execution_count": 36, "metadata": { "collapsed": false }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Ok\n" ] }, { "data": { "text/plain": [ "(0.012944936752319336, 262.47025990486145, 0.0013048648834228516)" ] }, "execution_count": 36, "metadata": {}, "output_type": "execute_result" } ], "source": [ "big_test(150)" ] }, { "cell_type": "code", "execution_count": 37, "metadata": { "collapsed": false }, "outputs": [], "source": [ "# big_test(200)" ] }, { "cell_type": "markdown", "metadata": { "collapsed": false }, "source": [ "Судя по времени выполнения, решение 3SAT задачки через ЦЛП — не лучшая затея." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "collapsed": false }, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "argv": [ "/usr/bin/python3", "-m", "ipykernel_launcher", "-f", "{connection_file}" ], "display_name": "Python 3 (ipykernel)", "env": {}, "language": "python", "metadata": { "debugger": false }, "name": "python3", "resource_dir": "/usr/share/jupyter/kernels/python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.11.6" } }, "nbformat": 4, "nbformat_minor": 4 }